\begin{tabbing}
$\forall$\=${\it es}$:ES, $l$:IdLnk, ${\it tg}$:Id, $B$:Type, $P$:(\{$e$:E$\mid$ loc($e$) $=$ source($l$) $\in$ Id \}$\rightarrow$Prop),\+
\\[0ex]$f$:(\{$e$:E$\mid$ loc($e$) $=$ source($l$) $\in$ Id \}$\rightarrow$$B$), ${\it ds}$:$x$:Id fp$\rightarrow$ Type.
\-\\[0ex]es{-}sends{-}iff2(${\it es}$;$l$;${\it tg}$;$B$;${\it ds}$;$e$.$P$($e$);$e$.$f$($e$)) $\in$ Prop
\end{tabbing}